Search Results

Documents authored by Vitek, Jan


Document
Complete Volume
LIPIcs, Volume 222, ECOOP 2022, Complete Volume

Authors: Karim Ali and Jan Vitek

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)


Abstract
LIPIcs, Volume 222, ECOOP 2022, Complete Volume

Cite as

36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 1-940, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@Proceedings{ali_et_al:LIPIcs.ECOOP.2022,
  title =	{{LIPIcs, Volume 222, ECOOP 2022, Complete Volume}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{1--940},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022},
  URN =		{urn:nbn:de:0030-drops-162276},
  doi =		{10.4230/LIPIcs.ECOOP.2022},
  annote =	{Keywords: LIPIcs, Volume 222, ECOOP 2022, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Karim Ali and Jan Vitek

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)


Abstract
Front Matter, Table of Contents, Preface, Conference Organization

Cite as

36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 0:i-0:xx, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{ali_et_al:LIPIcs.ECOOP.2022.0,
  author =	{Ali, Karim and Vitek, Jan},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{0:i--0:xx},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.0},
  URN =		{urn:nbn:de:0030-drops-162286},
  doi =		{10.4230/LIPIcs.ECOOP.2022.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Artifact
CodeDJ: Reproducible Queries over Large-Scale Software Repositories (Artifact)

Authors: Petr Maj, Konrad Siek¹, Alexander Kovalenko, and Jan Vitek

Published in: DARTS, Volume 7, Issue 2, Special Issue of the 35th European Conference on Object-Oriented Programming (ECOOP 2021)


Abstract
Analyzing massive code bases is a staple of modern software engineering research – a welcome side-effect of the advent of large-scale software repositories such as GitHub. Selecting which projects one should analyze is a labor-intensive process, and a process that can lead to biased results if the selection is not representative of the population of interest. One issue faced by researchers is that the interface exposed by software repositories only allows the most basic of queries. CodeDJ is an infrastructure for querying repositories composed of a persistent datastore, constantly updated with data acquired from GitHub, and an in-memory database with a Rust query interface. CodeDJ supports reproducibility, historical queries are answered deterministically using past states of the datastore; thus researchers can reproduce published results. To illustrate the benefits of CodeDJ, we identify biases in the data of a published study and, by repeating the analysis with new data, we demonstrate that the study’s conclusions were sensitive to the choice of projects.

Cite as

Petr Maj, Konrad Siek¹, Alexander Kovalenko, and Jan Vitek. CodeDJ: Reproducible Queries over Large-Scale Software Repositories (Artifact). In Special Issue of the 35th European Conference on Object-Oriented Programming (ECOOP 2021). Dagstuhl Artifacts Series (DARTS), Volume 7, Issue 2, pp. 13:1-13:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@Article{maj_et_al:DARTS.7.2.13,
  author =	{Maj, Petr and Siek¹, Konrad and Kovalenko, Alexander and Vitek, Jan},
  title =	{{CodeDJ: Reproducible Queries over Large-Scale Software Repositories (Artifact)}},
  pages =	{13:1--13:4},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2021},
  volume =	{7},
  number =	{2},
  editor =	{Maj, Petr and Siek¹, Konrad and Kovalenko, Alexander and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.7.2.13},
  URN =		{urn:nbn:de:0030-drops-140371},
  doi =		{10.4230/DARTS.7.2.13},
  annote =	{Keywords: Software, Mining Code Repositories, Source Code Analysis}
}
Document
CodeDJ: Reproducible Queries over Large-Scale Software Repositories

Authors: Petr Maj, Konrad Siek, Alexander Kovalenko, and Jan Vitek

Published in: LIPIcs, Volume 194, 35th European Conference on Object-Oriented Programming (ECOOP 2021)


Abstract
Analyzing massive code bases is a staple of modern software engineering research – a welcome side-effect of the advent of large-scale software repositories such as GitHub. Selecting which projects one should analyze is a labor-intensive process, and a process that can lead to biased results if the selection is not representative of the population of interest. One issue faced by researchers is that the interface exposed by software repositories only allows the most basic of queries. CodeDJ is an infrastructure for querying repositories composed of a persistent datastore, constantly updated with data acquired from GitHub, and an in-memory database with a Rust query interface. CodeDJ supports reproducibility, historical queries are answered deterministically using past states of the datastore; thus researchers can reproduce published results. To illustrate the benefits of CodeDJ, we identify biases in the data of a published study and, by repeating the analysis with new data, we demonstrate that the study’s conclusions were sensitive to the choice of projects.

Cite as

Petr Maj, Konrad Siek, Alexander Kovalenko, and Jan Vitek. CodeDJ: Reproducible Queries over Large-Scale Software Repositories. In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 6:1-6:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{maj_et_al:LIPIcs.ECOOP.2021.6,
  author =	{Maj, Petr and Siek, Konrad and Kovalenko, Alexander and Vitek, Jan},
  title =	{{CodeDJ: Reproducible Queries over Large-Scale Software Repositories}},
  booktitle =	{35th European Conference on Object-Oriented Programming (ECOOP 2021)},
  pages =	{6:1--6:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-190-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{194},
  editor =	{M{\o}ller, Anders and Sridharan, Manu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2021.6},
  URN =		{urn:nbn:de:0030-drops-140498},
  doi =		{10.4230/LIPIcs.ECOOP.2021.6},
  annote =	{Keywords: Software, Mining Code Repositories, Source Code Analysis}
}
Document
Artifact
On Julia’s Efficient Algorithm for Subtyping Union Types and Covariant Tuples (Artifact)

Authors: Benjamin Chung, Francesco Zappa Nardelli, and Jan Vitek

Published in: DARTS, Volume 5, Issue 2, Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019)


Abstract
This is the artifact for the pearl paper "On Julia’s efficient algorithm for subtyping union types and covariant tuples."

Cite as

Benjamin Chung, Francesco Zappa Nardelli, and Jan Vitek. On Julia’s Efficient Algorithm for Subtyping Union Types and Covariant Tuples (Artifact). In Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Dagstuhl Artifacts Series (DARTS), Volume 5, Issue 2, pp. 8:1-8:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@Article{chung_et_al:DARTS.5.2.8,
  author =	{Chung, Benjamin and Nardelli, Francesco Zappa and Vitek, Jan},
  title =	{{On Julia’s Efficient Algorithm for Subtyping Union Types and Covariant Tuples}},
  pages =	{8:1--8:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2019},
  volume =	{5},
  number =	{2},
  editor =	{Chung, Benjamin and Nardelli, Francesco Zappa and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.5.2.8},
  URN =		{urn:nbn:de:0030-drops-107855},
  doi =		{10.4230/DARTS.5.2.8},
  annote =	{Keywords: Type systems, subtyping, algorithmic type systems, distributive unions}
}
Document
Pearl
Julia’s Efficient Algorithm for Subtyping Unions and Covariant Tuples (Pearl)

Authors: Benjamin Chung, Francesco Zappa Nardelli, and Jan Vitek

Published in: LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)


Abstract
The Julia programming language supports multiple dispatch and provides a rich type annotation language to specify method applicability. When multiple methods are applicable for a given call, Julia relies on subtyping between method signatures to pick the correct method to invoke. Julia’s subtyping algorithm is surprisingly complex, and determining whether it is correct remains an open question. In this paper, we focus on one piece of this problem: the interaction between union types and covariant tuples. Previous work normalized unions inside tuples to disjunctive normal form. However, this strategy has two drawbacks: complex type signatures induce space explosion, and interference between normalization and other features of Julia’s type system. In this paper, we describe the algorithm that Julia uses to compute subtyping between tuples and unions - an algorithm that is immune to space explosion and plays well with other features of the language. We prove this algorithm correct and complete against a semantic-subtyping denotational model in Coq.

Cite as

Benjamin Chung, Francesco Zappa Nardelli, and Jan Vitek. Julia’s Efficient Algorithm for Subtyping Unions and Covariant Tuples (Pearl). In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 24:1-24:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{chung_et_al:LIPIcs.ECOOP.2019.24,
  author =	{Chung, Benjamin and Zappa Nardelli, Francesco and Vitek, Jan},
  title =	{{Julia’s Efficient Algorithm for Subtyping Unions and Covariant Tuples}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{24:1--24:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Donaldson, Alastair F.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.24},
  URN =		{urn:nbn:de:0030-drops-108165},
  doi =		{10.4230/LIPIcs.ECOOP.2019.24},
  annote =	{Keywords: Type systems, Subtyping, Union types}
}
Document
KafKa: Gradual Typing for Objects

Authors: Benjamin Chung, Paley Li, Francesco Zappa Nardelli, and Jan Vitek

Published in: LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)


Abstract
A wide range of gradual type systems have been proposed, providing many languages with the ability to mix typed and untyped code. However, hiding under language details, these gradual type systems embody fundamentally different ideas of what it means to be well-typed. In this paper, we show that four of the most common gradual type systems provide distinct guarantees, and we give a formal framework for comparing gradual type systems for object-oriented languages. First, we show that the different gradual type systems are practically distinguishable via a three-part litmus test. We present a formal framework for defining and comparing gradual type systems. Within this framework, different gradual type systems become translations between a common source and target language, allowing for direct comparison of semantics and guarantees.

Cite as

Benjamin Chung, Paley Li, Francesco Zappa Nardelli, and Jan Vitek. KafKa: Gradual Typing for Objects. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 12:1-12:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{chung_et_al:LIPIcs.ECOOP.2018.12,
  author =	{Chung, Benjamin and Li, Paley and Zappa Nardelli, Francesco and Vitek, Jan},
  title =	{{KafKa: Gradual Typing for Objects}},
  booktitle =	{32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
  pages =	{12:1--12:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-079-8},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{109},
  editor =	{Millstein, Todd},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.12},
  URN =		{urn:nbn:de:0030-drops-92170},
  doi =		{10.4230/LIPIcs.ECOOP.2018.12},
  annote =	{Keywords: Gradual typing, object-orientation, language design, type systems}
}
Document
KafKa: Gradual Typing for Objects (Artifact)

Authors: Benjamin Chung, Paley Li, Francesco Zappa Nardelli, and Jan Vitek

Published in: DARTS, Volume 4, Issue 3, Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018)


Abstract
A wide range of gradual type systems have been proposed, providing many languages with the ability to mix typed and untyped code. However, hiding under language details, these gradual type systems have fundamentally different ideas of what it means to be typed. In this paper, we show that four of the most common gradual type systems provide distinct guarantees, and we give a formal framework for comparing gradual type systems for object-oriented languages. First, we show that the different gradual type systems are practically distinguishable via a three-part litmus test. Then, we present a formal framework for defining and comparing gradual type systems. Within this framework, different gradual type systems become translations between a common source and target language, allowing for direct comparison of semantics and guarantees.

Cite as

Benjamin Chung, Paley Li, Francesco Zappa Nardelli, and Jan Vitek. KafKa: Gradual Typing for Objects (Artifact). In Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Dagstuhl Artifacts Series (DARTS), Volume 4, Issue 3, pp. 10:1-10:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@Article{chung_et_al:DARTS.4.3.10,
  author =	{Chung, Benjamin and Li, Paley and Nardelli, Francesco Zappa and Vitek, Jan},
  title =	{{KafKa: Gradual Typing for Objects (Artifact)}},
  pages =	{10:1--10:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2018},
  volume =	{4},
  number =	{3},
  editor =	{Chung, Benjamin and Li, Paley and Nardelli, Francesco Zappa and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.4.3.10},
  URN =		{urn:nbn:de:0030-drops-92411},
  doi =		{10.4230/DARTS.4.3.10},
  annote =	{Keywords: Gradual typing, object-orientation, language design, type systems}
}
Document
Parallelizing Julia with a Non-Invasive DSL (Artifact)

Authors: Todd A. Anderson, Hai Liu, Lindsey Kuper, Ehsan Totoni, Jan Vitek, and Tatiana Shpeisman

Published in: DARTS, Volume 3, Issue 2, Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017)


Abstract
This artifact is based on ParallelAccelerator, an embedded domain-specific language (DSL) and compiler for speeding up compute-intensive Julia programs. In particular, Julia code that makes heavy use of aggregate array operations is a good candidate for speeding up with ParallelAccelerator. ParallelAccelerator is a non-invasive DSL that makes as few changes to the host programming model as possible.

Cite as

Todd A. Anderson, Hai Liu, Lindsey Kuper, Ehsan Totoni, Jan Vitek, and Tatiana Shpeisman. Parallelizing Julia with a Non-Invasive DSL (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 7:1-7:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@Article{anderson_et_al:DARTS.3.2.7,
  author =	{Anderson, Todd A. and Liu, Hai and Kuper, Lindsey and Totoni, Ehsan and Vitek, Jan and Shpeisman, Tatiana},
  title =	{{Parallelizing Julia with a Non-Invasive DSL (Artifact)}},
  pages =	{7:1--7:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2017},
  volume =	{3},
  number =	{2},
  editor =	{Anderson, Todd A. and Liu, Hai and Kuper, Lindsey and Totoni, Ehsan and Vitek, Jan and Shpeisman, Tatiana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.3.2.7},
  URN =		{urn:nbn:de:0030-drops-72888},
  doi =		{10.4230/DARTS.3.2.7},
  annote =	{Keywords: parallelism, scientific computing, domain-specific languages, Julia}
}
Document
Parallelizing Julia with a Non-Invasive DSL

Authors: Todd A. Anderson, Hai Liu, Lindsey Kuper, Ehsan Totoni, Jan Vitek, and Tatiana Shpeisman

Published in: LIPIcs, Volume 74, 31st European Conference on Object-Oriented Programming (ECOOP 2017)


Abstract
Computational scientists often prototype software using productivity languages that offer high-level programming abstractions. When higher performance is needed, they are obliged to rewrite their code in a lower-level efficiency language. Different solutions have been proposed to address this trade-off between productivity and efficiency. One promising approach is to create embedded domain-specific languages that sacrifice generality for productivity and performance, but practical experience with DSLs points to some road blocks preventing widespread adoption. This paper proposes a non-invasive domain-specific language that makes as few visible changes to the host programming model as possible. We present ParallelAccelerator, a library and compiler for high-level, high-performance scientific computing in Julia. ParallelAccelerator's programming model is aligned with existing Julia programming idioms. Our compiler exposes the implicit parallelism in high-level array-style programs and compiles them to fast, parallel native code. Programs can also run in "library-only" mode, letting users benefit from the full Julia environment and libraries. Our results show encouraging performance improvements with very few changes to source code required. In particular, few to no additional type annotations are necessary.

Cite as

Todd A. Anderson, Hai Liu, Lindsey Kuper, Ehsan Totoni, Jan Vitek, and Tatiana Shpeisman. Parallelizing Julia with a Non-Invasive DSL. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 4:1-4:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{anderson_et_al:LIPIcs.ECOOP.2017.4,
  author =	{Anderson, Todd A. and Liu, Hai and Kuper, Lindsey and Totoni, Ehsan and Vitek, Jan and Shpeisman, Tatiana},
  title =	{{Parallelizing Julia with a Non-Invasive DSL}},
  booktitle =	{31st European Conference on Object-Oriented Programming (ECOOP 2017)},
  pages =	{4:1--4:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-035-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{74},
  editor =	{M\"{u}ller, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.4},
  URN =		{urn:nbn:de:0030-drops-72693},
  doi =		{10.4230/LIPIcs.ECOOP.2017.4},
  annote =	{Keywords: parallelism, scientific computing, domain-specific languages, Julia}
}
Document
Rethinking Experimental Methods in Computing (Dagstuhl Seminar 16111)

Authors: Daniel Delling, Camil Demetrescu, David S. Johnson, and Jan Vitek

Published in: Dagstuhl Reports, Volume 6, Issue 3 (2016)


Abstract
This report documents the talks and discussions at the Dagstuhl seminar 16111 "Rethinking Experimental Methods in Computing". The seminar brought together researchers from several computer science communities, including algorithm engineering, programming languages, information retrieval, high-performance computing, operations research, performance analysis, embedded systems, distributed systems, and software engineering. The main goals of the seminar were building a network of experimentalists and fostering a culture of sound quantitative experiments in computing. During the seminar, groups of participants have worked on distilling useful resources based on the collective experience gained in different communities and on planning actions to promote sound experimental methods and reproducibility efforts.

Cite as

Daniel Delling, Camil Demetrescu, David S. Johnson, and Jan Vitek. Rethinking Experimental Methods in Computing (Dagstuhl Seminar 16111). In Dagstuhl Reports, Volume 6, Issue 3, pp. 24-43, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@Article{delling_et_al:DagRep.6.3.24,
  author =	{Delling, Daniel and Demetrescu, Camil and Johnson, David S. and Vitek, Jan},
  title =	{{Rethinking Experimental Methods in Computing (Dagstuhl Seminar 16111)}},
  pages =	{24--43},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{6},
  number =	{3},
  editor =	{Delling, Daniel and Demetrescu, Camil and Johnson, David S. and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.6.3.24},
  URN =		{urn:nbn:de:0030-drops-61463},
  doi =		{10.4230/DagRep.6.3.24},
  annote =	{Keywords: Algorithms, Benchmarks, Data sets, Experiments, Repeatability, Reproducibility, Software Artifacts, Statistics}
}
Document
Concrete Types for TypeScript

Authors: Gregor Richards, Francesco Zappa Nardelli, and Jan Vitek

Published in: LIPIcs, Volume 37, 29th European Conference on Object-Oriented Programming (ECOOP 2015)


Abstract
Typescript extends JavaScript with optional type annotations that are, by design, unsound and, that the Typescript compiler discards as it emits code. This design point preserves programming idioms developers are familiar with, and allows them to leave their legacy code unchanged, while offering a measure of static error checking in parts of the program that have type annotations. We present an alternative design for TypeScript, one where it is possible to support the same degree of dynamism, but where types can be strengthened to provide hard guarantees. We report on an implementation, called StrongScript, that improves runtime performance of typed programs when run on a modified version of the V8 JavaScript engine.

Cite as

Gregor Richards, Francesco Zappa Nardelli, and Jan Vitek. Concrete Types for TypeScript. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 76-100, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{richards_et_al:LIPIcs.ECOOP.2015.76,
  author =	{Richards, Gregor and Zappa Nardelli, Francesco and Vitek, Jan},
  title =	{{Concrete Types for TypeScript}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{76--100},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-86-6},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{37},
  editor =	{Boyland, John Tang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.76},
  URN =		{urn:nbn:de:0030-drops-52185},
  doi =		{10.4230/LIPIcs.ECOOP.2015.76},
  annote =	{Keywords: Gradual typing, dynamic languages}
}
Document
Cooking the Books: Formalizing JMM Implementation Recipes

Authors: Gustavo Petri, Jan Vitek, and Suresh Jagannathan

Published in: LIPIcs, Volume 37, 29th European Conference on Object-Oriented Programming (ECOOP 2015)


Abstract
The Java Memory Model (JMM) is intended to characterize the meaning of concurrent Java programs. Because of the model's complexity, however, its definition cannot be easily transplanted within an optimizing Java compiler, even though an important rationale for its design was to ensure Java compiler optimizations are not unduly hampered because of the language's concurrency features. In response, Lea's JSR-133 Cookbook for Compiler Writers, an informal guide to realizing the principles underlying the JMM on different (relaxed-memory) platforms was developed. The goal of the cookbook is to give compiler writers a relatively simple, yet reasonably efficient, set of reordering-based recipes that satisfy JMM constraints. In this paper, we present the first formalization of the cookbook, providing a semantic basis upon which the relationship between the recipes defined by the cookbook and the guarantees enforced by the JMM can be rigorously established. Notably, one artifact of our investigation is that the rules defined by the cookbook for compiling Java onto Power are inconsistent with the requirements of the JMM, a surprising result, and one which justifies our belief in the need for formally provable definitions to reason about sophisticated (and racy) concurrency patterns in Java, and their implementation on modern-day relaxed-memory hardware. Our formalization enables simulation arguments between an architecture-independent intermediate representation of the kind suggested by Lea with machine abstractions for Power and x86. Moreover, we provide fixes for cookbook recipes that are inconsistent with the behaviors admitted by the target platform, and prove the correctness of these repairs.

Cite as

Gustavo Petri, Jan Vitek, and Suresh Jagannathan. Cooking the Books: Formalizing JMM Implementation Recipes. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 445-469, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{petri_et_al:LIPIcs.ECOOP.2015.445,
  author =	{Petri, Gustavo and Vitek, Jan and Jagannathan, Suresh},
  title =	{{Cooking the Books: Formalizing JMM Implementation Recipes}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{445--469},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-86-6},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{37},
  editor =	{Boyland, John Tang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.445},
  URN =		{urn:nbn:de:0030-drops-52334},
  doi =		{10.4230/LIPIcs.ECOOP.2015.445},
  annote =	{Keywords: Concurrency, Java, Memory Model, Relaxed-Memory}
}
Document
Foundations for Scripting Languages (Dagstuhl Seminar 12011)

Authors: Robert Hirschfeld, Shriram Krishnamurthi, and Jan Vitek

Published in: Dagstuhl Reports, Volume 2, Issue 1 (2012)


Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 12011 on the ``Foundations for Scripting Languages''. The choice of ``for'' rather than ``of'' is intentional: it is our thesis that scripting languages are in need of foundations to support their extensive use but lack them, and we hope this event consolidated and advanced the state of the art in this direction.

Cite as

Robert Hirschfeld, Shriram Krishnamurthi, and Jan Vitek. Foundations for Scripting Languages (Dagstuhl Seminar 12011). In Dagstuhl Reports, Volume 2, Issue 1, pp. 1-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


Copy BibTex To Clipboard

@Article{hirschfeld_et_al:DagRep.2.1.1,
  author =	{Hirschfeld, Robert and Krishnamurthi, Shriram and Vitek, Jan},
  title =	{{Foundations for Scripting Languages (Dagstuhl Seminar 12011)}},
  pages =	{1--18},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2012},
  volume =	{2},
  number =	{1},
  editor =	{Hirschfeld, Robert and Krishnamurthi, Shriram and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.2.1.1},
  URN =		{urn:nbn:de:0030-drops-34545},
  doi =		{10.4230/DagRep.2.1.1},
  annote =	{Keywords: scripting languages, programming languages semantics, type systems, verification techniques, security analyses, scalability, rapid software}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail